package var.satisfiability.rules;

import java.util.Iterator;

import tr.edu.ege.kipler.satisfiability.UnsatisfiableException;
import tr.edu.ege.kipler.satisfiability.blocking.BlockingStrategy;
import tr.edu.ege.kipler.satisfiability.completion.rules.RuleLogger;
import tr.edu.ege.kipler.satisfiability.completion.rules.dl.ABoxRule;
import tr.edu.ege.kipler.satisfiability.container.GenericABox;
import tr.edu.ege.kipler.satisfiability.container.Individual;
import tr.edu.ege.kipler.satisfiability.container.World;
import tr.edu.ege.kipler.satisfiability.container.WorldAccess;
import tr.edu.ege.kipler.syntax.KModality;
import tr.edu.ege.kipler.syntax.TypedModality;
import tr.edu.ege.kipler.syntax.WorldElement;
import tr.edu.ege.kipler.syntax.atomicformula.ConceptAssertion;
import tr.edu.ege.kipler.syntax.concept.Concept;
import tr.edu.ege.kipler.syntax.concept.ModalConcept;
import var.satisfiability.StrongBlockingStrategy;


public class DiamondConceptRule extends ABoxRule {

	private TypedModality operator;

	private GenericABox aBox;

	private boolean applied;

	private BlockingStrategy blockStrategy = new StrongBlockingStrategy();

	@Override
	public boolean isApplied() {
		return applied;
	}

	public DiamondConceptRule(TypedModality operator) {
		this.operator = operator;
	}

	public void apply() throws UnsatisfiableException {
		applied = false;
		aBox = getWorld().getABox();
		for (Iterator<Concept> i = getIndividual().conceptIterator(); i
				.hasNext();) {
			Concept concept = i.next();
			if (concept instanceof ModalConcept) {
				ModalConcept mc = (ModalConcept) concept;
				if (mc.getOperator() instanceof TypedModality
						&& mc.getOperator() instanceof KModality) {
					TypedModality modality = (TypedModality) mc.getOperator();
					if (!mc.getOperator().isNecessiate()
							&& modality.getType().equals(operator.getType())
							&& !blockStrategy.isBlocked(aBox, getIndividual()
									.getKey())
							&& !suchAWorldExists(mc, getIndividual())) {
						createAndConnectWorld(mc, getIndividual());
						applied = true;
					}
				}
			}
		}
	}

	private ConceptAssertion makeNewConAssert(ModalConcept modalDesc,
			Individual indv) {
		return new ConceptAssertion(modalDesc.getConcept(), indv.getKey()
				.toString());
	}

	protected boolean suchAWorldExists(ModalConcept modalDesc,
			Individual indv) {
		boolean conditionAlreadySatisfied = false;
		String relation = ((KModality) modalDesc.getOperator()).getRelation();
		WorldElement f = makeNewConAssert(modalDesc, indv);
		for (World world : getWcs().getAccWorldsByFrom(relation, getWorld())) {
			if (world.getABox().getFormulas().contains(f)) {
				conditionAlreadySatisfied = true;
				break;
			}
		}
		return conditionAlreadySatisfied;
	}

	protected World createAndConnectWorld(ModalConcept modalDesc,
			Individual indv) throws UnsatisfiableException {
		String relation = ((KModality) modalDesc.getOperator()).getRelation();
		World world = new World();
		ConceptAssertion newCa = makeNewConAssert(modalDesc, indv);
		world.add(newCa);
		getWcs().nameWorld(world);
		getWcs().addConstraint(new WorldAccess(getWorld(), world, relation));
		RuleLogger.getInstance().info(
				"WCS " + getWcs().getId() + " Diamond Concept Rule: Adding "
						+ newCa + " to the newly generated world "
						+ world.getName());
		return world;
	}

}
